Nuprl Lemma : eqmod_inversion
2,24
postcript
pdf
m
,
a
,
b
:
. (
a
=
b
mod
m
)
(
b
=
a
mod
m
)
latex
Definitions
a
=
b
mod
m
,
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
T
,
True
,
Prop
Lemmas
true
wf
,
squash
wf
,
divisor
of
minus
,
divides
wf
origin
m, a, b:
. (a = b mod m) 
(b = a mod m) m, a, b:. (a = b mod m) (b = a mod m) Qx:A. B(x)
T
T